package Datalog

case class DatalogRule(atoms: List[DatalogAtom], resolution: DatalogAtom) {
  val atomList = atoms
  val givenResolution = resolution

  def isDLRule(): Boolean = {
    // Check whether the arity of every atom is fine
    for (atom <- atoms if atom.pred.arity != 2 && atom.pred.arity != 1) return false

    if (resolution.pred.arity != 2 && resolution.pred.arity != 1) false
    else {

      val atomsArity2 = for (atom <- atoms if atom.pred.arity == 2) yield atom
      val startSet = makePaths(atomsArity2).toSet
      val onlyVariables = for (path <- startSet if path.start.isInstanceOf[Variable] && path.destination.isInstanceOf[Variable]) yield path

      if (onlyVariables.isEmpty) true // There are only constants
      else {
        val closure = combine(onlyVariables, onlyVariables)
        val pairs = for (path <- closure; path2 <- closure if path != path2) yield (path, path2)
        val booleans = pairs.map(a => a._2.isSimilarTo(a._1))

        !booleans.contains(true)
      }
    }
  }

  def makePaths(atoms: List[DatalogAtom]): List[DatalogPath] = atoms match {
    case Nil => Nil
    case x :: xs => new DatalogPath(x) :: makePaths(xs)
  }

  def combine(paths: Set[DatalogPath], copy: Set[DatalogPath]): Set[DatalogPath] = {
    val symmetric = symmetricClosure(paths, paths.toList)
    val transitive = transitiveClosure(symmetric, symmetric.toList)

    if (transitive == copy)
      combine(transitive, transitive)
    else
      transitive
  }

  def symmetricClosure(paths: Set[DatalogPath], copy: List[DatalogPath]): Set[DatalogPath] = copy match {
    case Nil => paths
    case x :: xs => symmetricClosure(paths + x.reverse, xs)
  }

  def transitiveClosure(paths: Set[DatalogPath], copy: List[DatalogPath]): Set[DatalogPath] = copy match {
    case Nil => paths
    case x :: xs => {
      val elements = findDestinationMatchesStart(x, paths)
      val newPaths = elements.map(element => x.combine(element))

      transitiveClosure(paths.union(newPaths.toSet), xs)
    }
  }

  def findDestinationMatchesStart(dest: DatalogPath, starts: Set[DatalogPath]): List[DatalogPath] = {
    val s = for {
      start <- starts.toList
      if dest.destination == start.start
    } yield start // search for an element, starting at the destination 

    if (s.isEmpty) null
    else s
  }

  override def toString() = "Atoms: " + atomList + "\tResolution: " + resolution
}
